An ongoing problem in the design of large systems is verifying that the system will behave in the manner as intended by its designers. One approach has been to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Since there is no guarantee that an untested system will work as expected, building the system itself can be an expensive proposition. Thus, those skilled in the art have migrated toward building and testing a model of the system through software.
A system model can be said to be a computer program or block of code that, when executed, simulates the intended properties (i.e. functions and/or features) of the system. The computer program, or system model, is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. Thus, by controlling the value of the system model inputs and monitoring the system model outputs, the functionality, or properties, of the system can be tested.
One method of testing a system model is called formal verification. In formal verification, the computer program (i.e. system model) is fed into a verification tool which converts the system model into a finite state machine. The finite state machine is a set of states and state transitions which mimic the operation of the system model in response to any given set of system model inputs. More specifically, each state represents a state the system model would enter given a set of inputs, and each state transition indicates the conditions (i.e. the value of system model inputs and system model variables) that must be met for the system model to transition from one state to another state.
A system model state machine can be used by the verification tool to test whether the system model behaves according to a set of expected behaviors (i.e. system properties). To do this, the verification tool controls and/or varies the system model inputs and monitors which states the system model enters as a result of the inputs. From this information, the verification tool can check whether the system model entered a state or a cycle of states which the designers of the system define as "bad" or unintended. If the system model enters a "bad" state or a "bad" cycle of states (i.e. repeatedly entering the same states over and over again), the system model is said to behave in a manner contradictory to that intended by the system designer.
Heretofore, in order to fully test every property or function of the system model through formal verification, the verification tool runs what is called a fall search of the system model state space (i.e. the set of states and transitions that comprise the system model state machine). A full search of a system model state space is a test wherein the system model inputs are varied such that each system model input takes on every value it can possibly assume during operation of the system model. That is, a fall search tests the behavior of the system model in response to every possible set of input values that the system model inputs can possibly assume when the system model is in operation. As a result, a full search insures that the system model behavior is tested under every set of conditions (i.e. every set of input values) that the system model can possibly undergo when in operation. Thus, a full search of a system model state space insures that every function, or property, of the system model is fully tested.
For example, a full search can be performed on a system model of a counter which increments a number, by one, up to ten each time it receives an input having a value of binary zero, and decrements the number, by one, down to zero each time it receives an input having a value of binary one. In such a system model, the numbers 0 through 10 represent the states the system model can enter, and the input values, binary zero and binary one, control the transitions between the states. When fully searching the system model, the search engine can start at a state representing the number 1 (i.e. state 1), vary As the input over the entire range of assumable values (i.e. binary one and binary zero) and identify the set of "next states" that the system model can possibly enter (e.g. state 0 when the input has a value of binary one, or state 2 when the input has a value of binary zero). Then, for each of the identified possible "next states," the inputs are again varied over the entire range of possible values to determine a new set of next states. This process is repeated until the search engine traces through the system model state space and determines that the system model can only enter a state (i.e. next state) that was already entered, or checked. Ultimately, if the full search finds that the system model did not enter an undesirable or "bad" state or set of states in response to a set of inputs, then the system model design is said to be error-free. That is, the system model is said to behave according to a design specification.
From this example, it is evident that running a full search to verify the behavior of a system model having one input with an assumable range of only two values (i.e. binary zero and binary one) can be an involved process, requiring a great deal of computational work. As a result, one can imagine that the more complex the system model becomes (i.e. the greater the number of system model inputs and/or the wider the range of assumable values for each input), the greater the chance that a computer-aided verification system will be incapable of handling the amount and/or complexity of the computations necessary to complete a full search. In fact, it has been found that verifying, or fully searching, such complex models with conventional verification tools can cause the verification tool to run out of computational resources (e.g. no more RAM available to the testing engine). When this happens, the verification tool may "lock-up" (i.e. stop the full search) without providing the tester with data as to whether the system model had behaved as expected for any part of the full search performed before the "lock-up." As a result, when fully searching such complex system models with conventional verification tools, the tester may be left with no way of determining whether the system model has a design error (i.e. can enter a "bad" state).
One solution to this problem is to reduce the size of the system model and run a full search of the reduced model. That is, a tester or programmer experienced in the details of the system model (i.e. how the system inputs and system variables affect the behavior of the system model) may eliminate portions of the system model (i.e. lines of code and/or system model inputs and variables) that appear to have no effect on a limited set of system properties (i.e. those system functions which the programmer decides are not critical to check). This may require, however, substantial time, effort and experience on the part of the programmer to insure that the system model is not reduced such that the reduced model fails to retain those portions that are critical for testing the designated set of system properties. In addition, although reducing the system model reduces the amount of computational resources required to check the system model, such a reduction prevents a full search from checking the behavior of all system model properties, or functions.